/LMAR=0/XLINE=3/FONT#3=BASB30/FONT#2=BASI30/FONT#1=BDR30/FONT#0=BDR30



␈↓ ↓H␈↓␈↓ ↓x␈↓αinst␈↓↓[␈↓αe␈↓↓, ␈↓αm␈↓↓, ␈↓αp␈↓↓] ←
␈↓ ↓H␈↓↓␈↓ α_␈↓βif␈↓↓ ␈↓αp␈↓↓ ␈↓βeq ␈↓↓NO ␈↓βthen␈↓↓ ␈↓αp
␈↓ ↓H␈↓α␈↓ α_␈↓βelse if␈↓↓ ␈↓βat ␈↓αm␈↓↓ ␈↓βthen␈↓↓
␈↓ ↓H␈↓↓␈↓ α8[␈↓βif␈↓↓ ␈↓αisvar␈↓↓ ␈↓αm␈↓↓ ␈↓βthen␈↓↓
␈↓ ↓H␈↓↓␈↓ αX{␈↓αassoc␈↓↓[␈↓αm␈↓↓, ␈↓αp␈↓↓]}[λ␈↓αw␈↓↓. ␈↓βif␈↓↓ ␈↓βn ␈↓αw␈↓↓ ␈↓βthen␈↓↓ [␈↓αm␈↓↓ . ␈↓αe␈↓↓] . ␈↓αp␈↓↓ ␈↓βelse if␈↓↓ ␈↓αequal␈↓↓[␈↓βd ␈↓αw␈↓↓, ␈↓αe␈↓↓] ␈↓βthen␈↓↓ ␈↓αp␈↓↓ ␈↓βelse␈↓↓ NO]
␈↓ ↓H␈↓↓␈↓ αA␈↓βelse if␈↓↓ ␈↓αm␈↓↓ ␈↓βeq ␈↓αe␈↓↓ ␈↓βthen␈↓↓ ␈↓αp
␈↓ ↓H␈↓α␈↓ αA␈↓βelse␈↓↓ NO]
␈↓ ↓H␈↓↓␈↓ α_␈↓βelse if␈↓↓ ␈↓βat ␈↓αe␈↓↓ ␈↓βthen␈↓↓ NO
␈↓ ↓H␈↓↓␈↓ α_␈↓βelse␈↓↓ ␈↓αinst␈↓↓[␈↓βd ␈↓αe␈↓↓, ␈↓βd ␈↓αm␈↓↓, ␈↓αinst␈↓↓[␈↓βa ␈↓αe␈↓↓, ␈↓βa ␈↓αm␈↓↓, ␈↓αp␈↓↓]]



␈↓ ↓H␈↓↓␈↓ ↓x␈↓αisvar␈↓↓ ␈↓αm␈↓↓ ← ␈↓αm␈↓↓ ε (U V W X Y Z)



␈↓ ↓H␈↓↓␈↓ ↓x␈↓αsublis␈↓↓[␈↓αe␈↓↓, ␈↓αp␈↓↓] ←
␈↓ ↓H␈↓↓␈↓ α_␈↓βif␈↓↓ ␈↓βat ␈↓αe␈↓↓ ␈↓βthen␈↓↓ {␈↓αassoc␈↓↓[␈↓αe␈↓↓, ␈↓αp␈↓↓]}[λ␈↓αw␈↓↓. ␈↓βif␈↓↓ ␈↓βn ␈↓αw␈↓↓ ␈↓βthen␈↓↓ ␈↓αe␈↓↓ ␈↓βelse␈↓↓ ␈↓βd ␈↓αw␈↓↓]
␈↓ ↓H␈↓↓␈↓ α_␈↓βelse␈↓↓ {␈↓αsublis␈↓↓[␈↓βa ␈↓αe␈↓↓, ␈↓αp␈↓↓], ␈↓αsublis␈↓↓[␈↓βd ␈↓αe␈↓↓, ␈↓αp␈↓↓]}[λ␈↓αx␈↓↓, ␈↓αy␈↓↓. ␈↓βif␈↓↓ ␈↓αx␈↓↓ ␈↓βeq a ␈↓αe␈↓↓ ∧ ␈↓αy␈↓↓ ␈↓βeq d ␈↓αe␈↓↓ ␈↓βthen␈↓↓ ␈↓αe␈↓↓ ␈↓βelse␈↓↓ ␈↓αx␈↓↓ . ␈↓αy␈↓↓]